T:Type, x,y:T, L:(T List).
(x  L)  (y  L)  (((x = y)  l_before(x; y; L; T))  l_before(y; x; L; T)) 

latex

Definitions	False, A, A  B, prop{i:l}, t  T, A c B, x:A. B(x), l_before(x; y; l; T), (x  l), P  Q, x:A. B(x), P  Q, ff, tt, if b then t else f fi , t  ...$L, ge(i; j), suptype(S; T), subtype(S; T), lelt(i; j; k), Y, increasing(f; k), P  Q, int_seg(i; j), sublist(T; L1; L2), ||as||, i <z j, b, i z j, nth_tl(n;as), hd(l), guard(T), sq_type(T), l[i], tl(l), True, T, P  Q, P  Q, , decidable(P), Unit, ,
Lemmas	nat wf, select wf, length wf1, decidable int equal, sublist wf, decidable lt, not functionality wrt iff, assert of bnot, eqff to assert, assert of eq int, eqtt to assert, iff transitivity, not wf, bnot wf, assert wf, bool wf, non neg length, length cons, length nil, increasing wf, le wf, int seg wf, eq int wf, ifthenelse wf, squash wf, select cons hd, select cons tl